1. $T$ : Type
\\[0ex]2. $T$ List
\\[0ex]3. $u$ : $T$
\\[0ex]4. $v$ : $T$ List
\\[0ex]5. $\forall$$x$:$T$. ($x$ $\in$ $v$) $\Rightarrow$ ($\neg$($x$ = last($v$))) $\Rightarrow$ $x$ before last($v$) $\in$ $v$
\\[0ex]$\vdash$  $\forall$$x$:$T$. ($x$ $\in$ [$u$ / $v$]) $\Rightarrow$ ($\neg$($x$ = last([$u$ / $v$]))) $\Rightarrow$ $x$ before last([$u$ / $v$]) $\in$ [$u$ / $v$]